-
Notifications
You must be signed in to change notification settings - Fork 227
Update pre-null-safety spec with new null safety sections #2023
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Conversation
|
An update fixing a few issues with interface types is on the way, will upload in half an hour, approx. ;-) |
|
Done. |
3829332 to
f5cb6da
Compare
|
Visit the preview URL for this PR (updated for commit 6cd9296): https://dart-specification--pr2023-specify-null-safety-56htdccy.web.app (expires Mon, 11 Jul 2022 14:42:40 GMT) 🔥 via Firebase Hosting GitHub Action 🌎 Sign: 6941ecd630c4f067ff3d02708a45ae0f0a42b88a |
f5cb6da to
24422fc
Compare
24422fc to
0fa020d
Compare
|
I skimmed over the changes and created the following checklist. I plan to review the text in parts and cross them out here when I'm done. The checklist itself may change in the future in case I missed anything.
|
|
I checked the part "Rules of Inference", in the green "after" column the lines range from 20728 to 20889. It looks good to me. EDIT: In my review I assumed that the requirement for the bounds of two function types is to be in the mutual-subtypes relationship. After a conversation with Erik I realized that the spec needs to be updated to mean that. |
|
I reviewed the part "Subsequent commentary" to the subtype algorithm, in the green "after" column the lines range from 20889 to 21291. I have two drive-by questions to the surrounding text. Otherwise, the part LGTM. |
|
I checked the part "Type Nullability", in the green "after" column the lines range from 21291 to 21414. I have left some comments, but otherwise LGTM. |
|
I checked the part "Top merge", in the green "after" column the lines range from 21414 to 21494. LGTM with one comment. |
|
I checked the part "IsTopType", in the green "after" column the lines range from 21494 to 21539. It LGTM. |
|
I checked the part "Moretop, morebottom", in the green "after" column the lines range from 21539 to 21582. LGTM. |
|
I checked the part "Type normalization", in the green "after" column the lines range from 21582 to 21737. LGTM with one question. |
|
I checked the part "Canonical syntax of types", in the green "after" column the lines range from 21737 to 21931. LGTM. |
specification/dartLangSpec.tex
Outdated
| \end{dartCode} | ||
|
|
||
| \commentary{% | ||
| No \emph{least} upper bound exists for \code{A} and \code{B}, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As I understand it, with the exception of a top type?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This particular sentence refers to the real, mathematical least upper bound in a set (Dart types) with an ordering relation (subtyping). The usage of 'least upper bound' in older versions of the spec is misleading, because it was never a least upper bound.
So we're looking for a type which is a supertype of both A and B, and it must be the least element among all the types which are supertypes of both A and B. It can't be I because we don't have I <: J; similarly it can't be J. But it also can't be a top type, because we don't have Top <: I (or J, or a bunch of other types).
So I think the claim is correct.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
But it also can't be a top type, because we don't have
Top <: I(orJ, or a bunch of other types).
I don't think I understand this argument. Shouldn't we have I <: Top and J <: Top (in the reverse order) in order to claim Top as the upper bound for both I and J?
Additionally, I think declarations class I {} and class J {} imply class I extends Object {} respectively class J extends Object {}, which makes Object an upper bound for A and B.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
True, Object is an upper bound for each of those classes, but that makes no difference: The least upper bound (mathematically speaking) of a set S of elements in an ordered set {v1, .. vk} is an element v from S that satisfies (1) vj <: v, for all j, and (v1 <: other && .. && vk <: other) => v <: other. It's the latter part that fails, so Top and Object aren't 'least', they are just upper bounds.
b9279cb to
6cd9296
Compare
|
The PR was rebased on the current |
6cd9296 to
66420dd
Compare
185037e to
ddd09ec
Compare
ddd09ec to
6c9de7a
Compare
ea307ec to
430eaf5
Compare
430eaf5 to
fb18232
Compare
8f0fb8e to
8322dc2
Compare
37e6c8b to
a955b79
Compare
a955b79 to
5263fa2
Compare
5263fa2 to
4ce96a8
Compare
8045a01 to
ad5ad39
Compare
ad5ad39 to
3192065
Compare
3192065 to
0b597cb
Compare
0b597cb to
85ec192
Compare
85ec192 to
9ebe10b
Compare
This PR was created by deleting the sections from
Subtypesto (but not including)Referenceplus the appendixAlgorithmic Subtyping, and inserting the sectionSubtypesfrom the null safety update branch plus all the following sections until (but not including)Reference, plus the new version of the appendixAlgorithmic Subtyping.The point is that this PR introduces a large chunk of the new material related to null safety which is introduced into the language specification, and it does not include all the small changes to sections that are mostly the same as before (those changes will be submitted as other PRs later on). In other words, the text before
Subtypingis unchanged (apart from the fixes mentioned below), and references from the new material to any location beforeSubtypingmay thus very well refer to obsolete language.A couple of other updates were necessary in order to make the result LaTeX'able:
dart.stywas updated to be the version used with the null safety PR (the new version includes a number of declarations that are used by the material about null safety).dartLangSpec.texwas updated to use\Deltarather than\Gammato denote a type variable environment (that's the common notation; we previously used\Gamma, but that's typically a "term" variable environment, so\Deltawould be less confusing for readers who also read research papers involving type systems).\RawFunctionTypeNamedwas updated to allow for therequiredmodifier; a couple of changes were necessary in sections beforeSubtypingin order to make dartLangSpec.tex LaTeX'able again, but this only involved adding the new LaTeX macro argument{r}, further updates will take place later on (this update just updates stuff fromSubtypingand out).\diamondto\triangle, because\triangleis now also used over=in order to indicate that a certain term of the formA = BdefinesA.\ominussymbol, similar to the symbolic traffic sign meaning "No entrance"), this symbol is used in the new material, that is, nowhere before sectionSubtyping; for instance, it occurs in sectionType Null.Unfortunately, the diff algorithm in git (and, probably, almost any diff algorithm) does not quite understand that the operation performed here is "delete two big chunks of text and insert replacements that are mostly new material", but it does seem to get on track after a while.